perm filename UNIQUE.LSP[W84,JMC] blob sn#747340 filedate 1984-03-18 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	unique.lsp[w84,jmc]	Try at circumscribing unique names in ekl
C00003 ENDMK
C⊗;
unique.lsp[w84,jmc]	Try at circumscribing unique names in ekl

(axiom |∀x.equal(x,x)|)

(axiom |∀x y.equal(x,y) ⊃ equal(y,x)|)

(axiom |∀x y z.equal(x,y) ∧ equal(y,z) ⊃ equal(x,z)|)

(axiom |∀P x y.denotational P ∧ P(x) ∧ equal(x,y) ⊃ P(y)|)

(axiom |∀x y. x ≠ y ∧ ¬ab aspect1(x,y) ⊃ ¬equal(x,y)|)
;;; We don't really need this if we circumscribe  equal  directly.